(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sk -> Sg *)

(* 水平面转动角度 φ   *)
Parameter phi  : R.

(* 对称面转动角度 μ ) *)
Parameter my  : R.

(* Sk在飞机对称面转动 μ度 得到S' *)
Definition coordinate_S'Sk :  Mat R 3 3 := mkMat_3_3
  (cos my)   0  (sin my)
     0       1    0
  (-sin my)  0  (cos my).

(* S'在水平面转动 φ度 到过度坐标系Sg *)
Definition coordinate_SgS' :  Mat R 3 3 := mkMat_3_3
  (cos phi)  (-sin phi)  0
  (sin phi)  (cos phi )  0
      0          0       1.

(* 最后可得到Sk到Sg的转换 *)
Definition coordinate_SkSg :  Mat R 3 3 := mkMat_3_3
  ((cos my)*(cos phi))  (-sin phi) ((sin my)*(cos phi))
  ((cos my)*(sin phi))  (cos phi)  ((sin my)*(sin phi))
  (-sin my)                 0      (cos my).

(* multiplication of S'Sk and SgS' *)
Definition mul_SgS'_S'Sk := 
  RMmul coordinate_SgS' coordinate_S'Sk.

(* verify S'Sk * SgS' = SgSk *)
Lemma SgS'_mul_S'Sk_eq_SkSg : 
    coordinate_SkSg === mul_SgS'_S'Sk.
Proof.
  unfold mul_SgS'_S'Sk.
  unfold coordinate_SkSg.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal2. ring. f_equal2. ring. f_equal. ring.
  f_equal2. ring.
Qed.
